COMMENT ⊗   VALID 00002 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	ideas[s88,jmc]
C00007 ENDMK
C⊗;
ideas[s88,jmc]

Relevant to YSP

There are reasons for propositions being true and reasons for believing
propositions.  Maybe success in YSP depends on keeping them distinct.
There might be a reason for the gun to become unloaded, but there is
no reason for believing the gun became unloaded.

If we have  p ∨ q in our database, then minimization of both  p  and  q
would tell us that exactly one is true.  However, minimization of beliefs
tells us that we have no reason to believe  p  and no reason to believe
q,  even though we have a reason to believe  p ∨ q.

How does one say, ``I don't know of an event that unloads the gun.''?

Maybe to minimize the number of unknown events two circumscriptions
are required --- one the usual minimization of  $ab$ that gives two
models in YSP and a second involving knowledge that selects among them.

Can we do the above in autoepistemic logic or in VAL's introspective
circumscription?

causes(wait,unload,r(load,S0))

New form of common sense law of inertia:

inertial p ∧ holds(p,s) ∧ ¬causes(e,not p,s) ⊃ holds(p,r(e,s))

The following form for general fluents seems better:

inertial f ∧ ¬changes(e,f,s) ⊃ value(f,r(e,s)) = value(f,s)

We'll have  $inertial alive$ and $inertial loaded$.

To infer

holds(loaded,r(wait,r(load,S0)))

or

value(loaded,r(wait,r(load,S0))) = true

We need to formalize ``I don't know any reason for $wait$ to change loaded
in $r(load,S0)$.''  Why can't we make it, ``I don't know any reason for

$$value(loaded,r(wait,r(load,S0))) ≠ value(loaded,r(load,S0)))?''$$

june 22 - discussed it with Arkady

Here's a propositional version of the problem.

Introduce

1. a unary predicate $supported(p)$ which means that the proposition
$p$ is supported.

2. a binary predicate $supports(p,q)$ which means that if the proposition
$p$ is supported, so is $q$.

We have the axiom

$$supported(taut)$$

for all tautologies $taut$.

We have the transitive law

$$supported(p) ∧ supports(p,q) ⊃ supported(q)$$.

I suppose we also want modus ponens for support in the form

$$supported(p) ∧ supported(p implies q) ⊃ supported(q).$$

The Yale shooting problem, reduced to its propositional essentials,
involves two propositions

$P$ standing for $value(loaded,r(wait,r(load,S0))) = true$, and

$Q$ standing for $value(alive,r(shoot,r(wait,r(load,S0)))) = true$.

We have as axioms for YSP itself

$$supported(P),$$

$$supported(Q),$$
%
and
%
$$supports(Q,not(P)).$$

The predicate $supported$ is circumsribed with just itself as variable.
Actually, supported looks like the modal $necessary$, provided we take
the axioms about the particular situation as necessary.

We have the further definition

$$∀p(anomalous(p) ≡ true(p) ∧ (¬supported(p) ∨ supported(not(p)))).$$

Our idea is to the circumscribe anomalous propositions.

It looks like the intended model in which we have $true(Q) ∧ true(not P)$
has no anomalies, and the other model has one.